k:Knd, l:IdLnk, dt:fpf(Id; x.Type).
(fpf-dom(Kind-deq; k; lnk-decl(l; dt)))
 sqequal(fpf-ap(lnk-decl(l; dt); Kind-deq; k); fpf-ap(dt; id-deq; tag(k))) 

latex

Definitions	tag(k), x:A  B(x), left + right, Knd, t  T, IdLnk, Id, Type, x. t(x), x:A. B(x), fpf(A; a.B(a)), lnk-decl(l; dt), x.A(x), top, x:AB(x), Kind-deq, fpf-dom(eq; x; f), b, P  Q, guard(T), sq_type(T), s = t, prop{i:l}, sqequal(s; t), False, A, b, , id-deq, rcv(l,tg), P  Q, P  Q, Unit, fpf-cap(f; eq; x; z), void
Lemmas	lnk-decl-dom-not, lnk-decl-cap, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, rcv wf, id-deq wf, bool wf, bnot wf, not wf, lnk-decl-dom2, IdLnk sq, lnk-decl-dom, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, lnk-decl wf, fpf wf, Id wf, IdLnk wf, Knd wf